FDL - Step of Proof: fseg

Step of Proof: fseg_append

11,40

Inference at *
Iof proof for Lemma fseg append:

T:Type, l1, l2, l3:(T List). fseg(T;l1;l2)

fseg(T;l1;l3 @ l2)

by ((((Unfold `fseg` 0)

CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n

C)) (first_tok :t) inil_term)))

)

CollapseTHEN (((ExRepD)

CollapseTHEN (((((InstConcl [l3 @ L])

THENM (((WeakSubstFor l2 0)
THENM (RWO "append_assoc" 0))

))

)
TCollapseTHENA (Auto

))

))
TC

TC.

Definitions as @ bs, fseg(T;L1;L2), x:A. B(x), A List, [], i j , A B, [car / cdr], SQType(T), {T}, s ~ t, , S T, Top, x:A.B(x), Void, {x:A| B(x)} , ||as||, , P Q, P & Q, x:A B(x), P Q, P Q, Type, , type List, x:A. B(x), x:AB(x), s = t, t T

Lemmas non neg length, cons one one, guard wf, nat wf, length wf nat, top wf, member wf, iff wf, rev implies wf, append assoc, append wf

Definitions	as @ bs, fseg(T;L1;L2), x:A. B(x), A List, [], i j , A B, [car / cdr], SQType(T), {T}, s ~ t, , S T, Top, x:A.B(x), Void, {x:A\| B(x)} , \|\|as\|\|, , P Q, P & Q, x:A B(x), P Q, P Q, Type, , type List, x:A. B(x), x:AB(x), s = t, t T
Lemmas	non neg length, cons one one, guard wf, nat wf, length wf nat, top wf, member wf, iff wf, rev implies wf, append assoc, append wf